\begin{tabbing}
$\forall$$i$:Id, $a$:Atom1, $k$:Knd, $A$:MsgA.
\\[0ex]AtomFree(ds($A$))
\\[0ex]$\Rightarrow$ AtomFree(da($A$))
\\[0ex]$\Rightarrow$ \=$\lambda$$z$,${\it z@}_{0}$. filter($\lambda$$m$.source(mlnk($m$)) = $i$;$A$.sends($k$,$z$,${\it z@}_{0}$)):$A$.state$\rightarrow$$A$.da($k$)$\rightarrow$\+
\\[0ex](\{$m$:Msg($\lambda$$l$,${\it tg}$. $A$.dout($l$,${\it tg}$))$\mid$ source(mlnk($m$)) $=$ $i$ \} List)$>>$$a$
\-\\[0ex]$\Rightarrow$ ma{-}body($A$):Shape($A$)$>>$$a$
\end{tabbing}